\documentclass{beamer}
 \usepackage{import}
\usepackage{bussproofs}
% \import{../}{k2latex.bb.sty}

\usepackage{amssymb,amscd}
\usepackage{amsmath}
\usepackage{stmaryrd}
\usepackage{bm}
\usepackage{xparse}
\usepackage{tikz}
\usetikzlibrary{matrix,arrows,decorations.pathmorphing}
\usepackage{algorithm}
\usepackage{algpseudocode}
\usepackage{ifpdf}
\usepackage{rotating}


\usepackage{pgf}
\usetheme{CambridgeUS}
%\logo{\includegraphics[height=0.5cm,width=1cm]{circ.png}}
\usecolortheme{dolphin}

\newcommand{\parto}{\rightharpoondown}
\newcommand{\ltrans}[1]{\xrightarrow{#1}}

\newcommand{\Cfg}{\mathit{Cfg}}
\newcommand{\CfgSym}{\mathit{Cfg}^{s}}
\newcommand{\Bool}{\mathit{Bool}}
\newcommand{\true}{\mathit{true}}
\newcommand{\false}{\mathit{false}}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\eqbydef}{\triangleq}
\newcommand{\A}{\mathcal{A}}
\renewcommand{\L}{\mathcal{L}}
\renewcommand{\S}{\mathcal{S}}
%\newcommand{\G}{\mathcal{G}}
\newcommand{\G}{G}
\newcommand{\R}{\mathcal{R}}
\newcommand{\T}{\mathcal{T}}
\newcommand{\D}{\mathcal{D}}
\newcommand{\Var}{\mathit{Var}}
\newcommand{\var}{\mathit{var}}
\newcommand{\sym}{\mathit{\Delta}}
\newcommand{\SymVar}{\mathit{Val^{\mathfrak{s}}}}
\DeclareDocumentCommand{\TSym}{g}{{\T}^{s}\IfNoValueF {#1} {_{#1}}}
\newcommand{\SSym}{{\S}^{s}}
\newcommand{\Free}{\mathit{Free}}
\newcommand{\IMP}{\textsc{IMP}\xspace}
\newcommand{\sat}{\mathtt{sat}}
\newcommand{\unsat}{\mathtt{unsat}}
\newcommand{\asat}{\mathtt{sat}_{\approx}}
\newcommand{\aunsat}{\mathtt{unsat}_{\approx}}
\newcommand{\wsem}[1]{(\![{#1}]\!)}
\newcommand{\ssem}[1]{[\![{#1}]\!]}
\newcommand{\tran}[2]{\Ra^{#1}_{#2}}
\newcommand{\ltran}[3]{\stackrel{#1}{\Rightarrow}\stackrel{#2}{_{#3}}}
\newcommand{\pattern}[2]{{#1}%
  \ifthenelse{\equal{#2}{}}{}{%
    {\wedge}{#2}%
  }%
}
\newcommand{\foland}{\pmb{\land}}
\newcommand{\folor}{\pmb{\lor}}
\newcommand{\folneg}{\pmb{\neg}\,}
\newcommand{\vcirc}{\vdash^\circlearrowleft}
\renewcommand{\implies}{\longrightarrow}

\newcommand{\sTop}[1]{{#1}^{\mathfrak{p}}}
\newcommand{\pTos}[1]{{#1}^{\mathfrak{s}}}
\newcommand{\symb}[1]{{#1}^{\mathfrak{s}}}
\newcommand{\patt}[1]{{#1}^{\mathfrak{p}}}


\newcommand{\rrule}[3]{{#1}%
  \ifthenelse{\equal{#3}{}}{}{%
    \pmb{\wedge}{#3}%
  }%
  \pmb{\Rightarrow}{#2}
}


\newcommand{\symded}{\mathbin{\symb{\vdash}}}
\newcommand{\rlded}{\vdash}

% most used
\newcommand{\alphasym}{\pTos{\alpha}}
\newcommand{\sigmasym}{\pTos{\sigma}}
\newcommand{\pisym}{\pTos{\pi}}
\newcommand{\phisym}{\pTos{\phi}}

\definecolor{myviolet}{rgb}{.82, .0 ,.76}
\definecolor{myOliveGreen}{rgb}{1., .25 ,.0}
\definecolor{mymyviolet}{rgb}{.01, .72 ,.625}
\definecolor{mygrey}{rgb}{.6, .6 ,.6}
\definecolor{myyellow}{rgb}{.75, .8 ,.0}
\definecolor{mygreen}{rgb}{.2, .8 ,.0}
\definecolor{OliveGreen}{rgb}{.0, 0.48, 0.0}
\definecolor{myviolet}{rgb}{.9, .0 ,.4}

\definecolor{darkgreen}{rgb}{0,0.4,0}


\newcommand{\mycomment}[1]{}


\title[Symbolic Execution]
      {A Generic Framework for Symbolic Execution}

\author[A. Arusoaie, V. Rusu, D. Lucanu]{
{Andrei Arusoaie, Vlad Rusu, Dorel Lucanu}
}
\date{01/04/2013}
\institute[INRIA Lille, FII - UAIC]
{
\begin{tabular}{ll}
INRIA & Faculty of Computer Science\\
Lille, France & Alexandru Ioan Cuza University, Ia\c{s}i, Romania\\
{\tt vlad.rusu@inria.fr} &{\tt \{andrei.arusoaie, dlucanu\}@info.uaic.ro}
\end{tabular}
}

\begin{document}

\begin{frame}
\titlepage
\end{frame}

\AtBeginSection[]
{
  \begin{frame}<beamer>
    \frametitle{Plan}
    \tableofcontents[currentsection,currentsubsection]
  \end{frame}
}

\section*{Outline}
\begin{frame}
\tableofcontents
\end{frame}

\section{Language Definitions}

\begin{frame}{Main Ingredients for a Language Definition}
\begin{itemize}
\item syntax: BNF
\item semantics: $\L=(\Cfg, \Sigma,\Pi,\T,\S)$
\begin{itemize}
\item $(\Sigma,\Pi)$ a many-sorted first-order signature
\item $\Cfg$ - the sort for configurations
\item $\T$ a $(\Sigma,\Pi)$-model
\item $\S$ a set of reachability formulas $\rrule{\pattern{\pi}{\phi}}{\pattern{\pi'}{\phi'}}{}$
\end{itemize}
\end{itemize}
\end{frame}

\begin{frame}{Important Subsignatures}
For a language $\L$ we consider the following subsignatures:
\begin{itemize}
\item $(\Sigma^{\it Data},\Pi^{\it Data})$: integers, booleans, maps,
  sets, lists
\item $(\Sigma^{\L},\Pi^{\L})$: the syntax of $\L$ and its associated
  predicates (if any)
\end{itemize}
\end{frame}


\begin{frame}{On The Model $\T$ }
\begin{itemize}
\item we assume a $(\Sigma^{\it Data},\Pi^{\it Data})$-model $\D$
\item $\T$ extends $\D$ with term-like
  interpretations for the rest of functions:
\\
if $f\in\Sigma\setminus\Sigma^{\it Data}$,
$\T_{f(t_1,\ldots,t_n)}=f(\T_{t_1},\ldots,\T_{t_n})$
\end{itemize}
\end{frame}

\section{Symbolic Definition $\symb{\L}$}

\begin{frame}{A Symbolic Definition for $\L$}

We associate a new definition $\symb{\L}=(\symb{\Cfg}, \symb{\Sigma},\symb{\Pi},\symb{\T},\symb{\R})$ with $\L$ such that:

\begin{itemize}
\item some components of $\L$ can be symbolically represented (using
  logical variables)
\item a configuration is the term representation $\langle\symb{\pi},\symb{\phi}\rangle$ of a matching logic
  formula $\pattern{\pi}{\phi}$
\item the transition system $\tran{}{\L}$ and $\tran{}{\symb{\L}}$ are
    strong related:\\
\textcolor{myviolet}{for all} \textcolor{OliveGreen}{there is}\\
\centerline{
\begin{tikzpicture}[scale=1.5]
\node (A) at (0,1) {\textcolor{myviolet}{$\langle \pi^{\mathfrak{s}}, \phi^{\mathfrak{s}}\rangle$}};
\node (TS) at (1,1) {\textcolor{OliveGreen}{$\ltran{\alpha^{\mathfrak{s}}}{}{\symb{\L}}$}};
\node (B) at (2,1) {\textcolor{OliveGreen}{$\langle \pi'^{\mathfrak{s}}, \phi'^{\mathfrak{s}}\rangle$}};
%\node (M1) at (0,0.5) {\textcolor{myviolet}{\scriptsize $\models$}};
\node (M1) at (0,0.5) {\textcolor{myviolet}{\scriptsize \begin{sideways}$\models$\end{sideways}}};
%\node (M2) at (2,0.5) {\textcolor{OliveGreen}{\scriptsize $\models$}};
\node (M2) at (2,0.5) {\textcolor{myviolet}{\scriptsize \begin{sideways}$\models$\end{sideways}}};
\node (C) at (0,0) {\textcolor{myviolet}{$\gamma$}};
\node (T) at (1,0) {\textcolor{myviolet}{$\ltran{\alpha}{}{\L}$}};
\node (D) at (2,0) {\textcolor{myviolet}{$\gamma'$}};
\end{tikzpicture}
\qquad 
\begin{tikzpicture}[scale=1.5]
\node (A) at (0,1) {\textcolor{myviolet}{$\langle \pi^{\mathfrak{s}}, \phi^{\mathfrak{s}}\rangle$}};
\node (TS) at (1,1) {\textcolor{myviolet}{$\ltran{\alpha^{\mathfrak{s}}}{}{\symb{L}}$}};
\node (B) at (2,1) {\textcolor{myviolet}{$\langle \pi'^{\mathfrak{s}}, \phi'^{\mathfrak{s}}\rangle$}};
%\node (M1) at (0,0.5) {\textcolor{OliveGreen}{\scriptsize $\models$}};
\node (M1) at (0,0.5) {\textcolor{myviolet}{\scriptsize \begin{sideways}$\models$\end{sideways}}};
%\node (M2) at (2,0.5) {\textcolor{myviolet}{\scriptsize $\models$}};
\node (M2) at (2,0.5) {\textcolor{myviolet}{\scriptsize \begin{sideways}$\models$\end{sideways}}};
\node (C) at (0,0) {\textcolor{OliveGreen}{$\gamma$}};
\node (T) at (1,0) {\textcolor{OliveGreen}{$\ltran{\alpha}{}{\L}$}};
\node (D) at (2,0) {\textcolor{myviolet}{$\gamma'$}};
\end{tikzpicture}
}
$\gamma\models\langle\symb{\pi},\symb{\phi}\rangle$ iff there is $\rho$ s.t. $\gamma=\rho(\pi)$ and $\rho\models\phi$
\item only symbolic stuff can be sent to SMT solver (or other reasoner)
\end{itemize}


\end{frame}


\begin{frame}{Symbolic Execution Levels}
We see (at least) three levels at which the symbolic stuff is handled:
\begin{itemize}
\item \structure{data level}: $(\Sigma^{\it Data},\Pi^{\it Data})$ is interpreted
  on a symbolic domain $\symb{\D}$ that extends $\D$ with (logical)
  variables, called \emph{symbolic values}
\item \structure{data$+$language level}: extends data level with symbolic
  values denoting (pieces of) programs in $\L$
\item \structure{full level}: everything can be symbolic 
\end{itemize}
\alert{Here we deal only with data level!}
\begin{itemize}
\item $\symb{\S}=\{\rrule{\langle\symb{\pi},\Psi\rangle}{\langle\symb{\pi},\Psi\land\symb{\phi}\land\symb{\phi'}\rangle}{} \mid\rrule{\pattern{\pi}{\phi}}{\pattern{\pi'}{\phi'}}{}\in\S\}$
\end{itemize}
\end{frame}


\section{Symbolic Execution as a Proof System}

\begin{frame}{One Symbolic Step }
\vspace{-3ex}
\begin{align*}
\textsf{[Axiom]}~&\dfrac{\rrule{\pi \land \phi}{\varphi}{} \in \S}
  					{\S \symded \rrule{\pi}{\varphi \land \phi}{}}\\ 
\textsf{[Substitution]}~&\dfrac{\S \symded \rrule{\varphi}{\varphi'}{} \hspace{.5cm} , \hspace{.5cm} \sigma:\Var\to T_\Sigma(\Var) \hspace{5pt} substitution}{\S \symded \rrule{\sigma(\varphi)}{\sigma(\varphi')}{}} \\\textsf{[LogicalFraming]}~&\dfrac{\S \symded \rrule{\varphi}{\varphi'}{} \hspace{.5cm} , \hspace{.5cm} \phi \hspace{5pt} FOL~formula}{\S \symded \rrule{\varphi \land \phi}{\varphi' \land \phi}{}}
\end{align*}
\begin{theorem} 1. If $\S \symded \rrule{\pattern{\pi}{\phi}}{\pattern{\pi'}{\phi'}}{} $ then $\langle\symb{\pi},\symb{\phi}\rangle\tran{}{\symb{\L}}\langle\symb{\pi},\symb{\phi'}\rangle$.\\
2. If $\langle\symb{\pi},\symb{\phi}\rangle\tran{}{\symb{\L}}\langle\symb{\pi'},\symb{\phi'}\rangle$ then there is
$\S \symded \rrule{\pattern{\pi_0}{\phi_0}}{\pattern{\pi'_0}{\phi'_0}}{} $ and $\symb{\varrho}:\symb{\Var}\to\symb{\D}$ such that $\pattern{\pi}{\phi}=\varrho(\pattern{\pi_0}{\phi_0})$ and $\pattern{\pi'}{\phi'}=\varrho(\pattern{\pi'_0}{\phi'_0})$.
\end{theorem}
\end{frame}

\begin{frame}{Derivative}
\begin{definition}[Derivative]
\label{def:deriv}
For a set of semantical rules $\S$ and an elementary pattern $\varphi$, the derivative $\Delta_\S(\varphi)$ is the disjunction of the formulas that can be derived from $\varphi$ using $\symded$ , i.e.,  $\Delta_\S(\varphi) \eqbydef \bigvee_{\S \symded \rrule{\varphi}{\varphi'}{}} \varphi'$.\\
 For a  pattern $\bigvee_i \varphi_i$ with $\varphi_i$  elementary for all $i$,  $\Delta_\S(\bigvee_i \varphi_i) \eqbydef \bigvee_i \Delta_\S(\varphi_i)$.
\\ 
If $\rrule{\varphi}{\varphi'}{}$ is a reachability formula, then $\Delta_\S(\rrule{\varphi}{\varphi'}{})= \rrule{\Delta_\S(\varphi)}{\varphi'}{}$
\end{definition}

\begin{definition}
\label{d:total}
We say that $\S$ is \emph{weakly well-definable} if for any derivable pattern $\pi$, $\Delta_\S(\pi)$ is {\it weakly well-defined}.
\end{definition}

\begin{definition}[Derivable Pattern]
  An elementary pattern $\varphi \eqbydef \pi \wedge \phi$ is derivable for $\S$  if $\Delta_\S(\varphi)$ is nonempty.
 \end{definition}
\end{frame}

\begin{frame}{Properties for Weakly-well Definable Definitions}

\begin{lemma}
\label{l:sound-der}
If $\S$ is weakly well-definable and $\varphi\eqbydef\pi\land\phi$ is derivable then $\S \models \rrule{\varphi}{\Delta_\S(\varphi)}{}$.
\end{lemma}

\begin{lemma}
If $\S$ is weakly well-definable then there is ${\S}^\Delta$ weakly well-defined such that if ${\S}^\Delta\rlded\rrule{\varphi}{\varphi'}{}$ then  ${\S}\models\rrule{\varphi}{\varphi'}{}$.
\end{lemma}


\begin{theorem}
\label{prop:cc}
If $\S$ is weakly well-definable and $G$ is derivable for $\S$, then $\S^\Delta \cup G \rlded \sym_\S(G)$ implies $\S \models G$.
\end{theorem}

\end{frame}



\end{document}

\begin{frame}{A Name}

\end{frame}


\begin{itemize}
\item
\end{itemize}

\begin{verbatim}

\end{verbatim}
